FDL - Step of Proof: dec_iff_ex

Step of Proof: dec_iff_ex_bvfun

12,41

Inference at * 1
Iof proof for Lemma dec iff ex bvfun:

1. T : Type
2. E : T

x, y:T. Dec(E(x,y))

f:T

. (

x, y:T. (

(f(x,y)))

(E(x,y)))

by ((((((RenameVar `g' 3)

CollapseTHENM (Unfold `decidable` 3))

)

CollapseTHENM (((With

x,y.

Ccase g(x,y) of inl(a) => tt | inr(b) => ff (D 0))

CollapseTHENA ((Auto_aux (first_nat 1:n

C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

))

)

CollapseTHENM (Reduce 0))

C1:

C1: 3. g :

x, y:T. (E(x,y))

(

(E(x,y)))

C1:

x, y:T. (

case g(x,y) of inl(a) => tt | inr(b) => ff)

(E(x,y))

Definitions P Q, P Q, P & Q, t T, P Q, P Q, x:A. B(x), x:A. B(x), , Dec(P)

Lemmas assert wf, iff wf, bfalse wf, btrue wf, not wf

Definitions	P Q, P Q, P & Q, t T, P Q, P Q, x:A. B(x), x:A. B(x), , Dec(P)
Lemmas	assert wf, iff wf, bfalse wf, btrue wf, not wf